Inference at * 
Iof proof for Lemma all quot elim:


  T:Type, E:(TT).
  EquivRel(T;x,y.E(x,y))
   (F:((x,y:T//E(x,y))).
   (w:(x,y:T//E(x,y)). SqStable(F(w)))  ((z:(x,y:T//E(x,y)). F(z))  (z:T. F(z)))) 

latex

 by Unfold `so_apply` 0 

latex

 1: 

 1:   T:Type, E:(TT).
 1:   EquivRel(T;x,y.E(x,y))
 1:    (F:((x,y:T//(E(x,y)))).
 1:    (w:(x,y:T//(E(x,y))). SqStable(F(w)))
 1:     ((z:(x,y:T//(E(x,y))). F(z))  (z:T. F(z))))
 .

Definitions

x(s), x(s1,s2)